NIL 


(DEFPROP DOC 
 (NIL !BEGIN
      (!ASSIGN P (!PLUS (!MINUS V E) N))
      (!IF (!LE 1 E)
	   (!BEGIN (!SIMPLE-ASSIGN K K_FORUNDEFINED)
		   (!WHILE (!AND (!LE K_FORLOW K) (!LE K (!PLUS K_FORHIGH 1)))
			   (!LE K K_FORHIGH)
			   (!BEGIN (!ASSIGN K (!PLUS K 1))
				   (!IF_ELSE (!EQ (!CONCAT VA (!ARRAY_INDEX I)) 0)
					     (!BEGIN (!IF_ELSE (!EQ (!CONCAT VA (!ARRAY_INDEX J)) 0)
							       (!BEGIN (!ASSIGN (!CONCAT VA (!ARRAY_INDEX I))
 										C)
								       (!ASSIGN (!CONCAT VA (!ARRAY_INDEX J))
 										C)
								       (!ASSIGN C (!PLUS C 1)))
							       (!ASSIGN (!CONCAT VA (!ARRAY_INDEX I))
									(!CONCAT VA (!ARRAY_INDEX J))))
						     (!ASSIGN (!CONCAT T (!ARRAY_INDEX (!MINUS K N))) K))
					     (!IF_ELSE (!EQ (!CONCAT VA (!ARRAY_INDEX J)) 0)
						       (!BEGIN (!ASSIGN (!CONCAT VA (!ARRAY_INDEX J))
									(!CONCAT VA (!ARRAY_INDEX I)))
							       (!ASSIGN (!CONCAT T (!ARRAY_INDEX (!MINUS K N)))
 									K))
						       (!IF_ELSE (!NEQ (!CONCAT VA (!ARRAY_INDEX I))
								       (!CONCAT VA (!ARRAY_INDEX J)))
								 (!BEGIN (!IF (!LE 1 N)
									      (!BEGIN
									       (!SIMPLE-ASSIGN
										R
										R_FORUNDEFINED)
									       (!WHILE
										(!AND
										 (!LE R_FORLOW R)
										 (!LE R (!PLUS R_FORHIGH 1)))
										(!LE R R_FORHIGH)
										(!BEGIN
										 (!ASSIGN R (!PLUS R 1))
										 (!IF
										  (!EQ
										   (!CONCAT VA
											    (!ARRAY_INDEX R))
										   J)
										  (!ASSIGN
										   (!CONCAT VA
											    (!ARRAY_INDEX R))
										   I))))
									       (!ASSIGN R_FORHIGH N)
									       (!ASSIGN R R_FORLOW)
									       (!ASSIGN R_FORLOW 1)))
									 (!ASSIGN J
										  (!CONCAT VA
											   (!ARRAY_INDEX J)))
									 (!ASSIGN I
										  (!CONCAT VA
											   (!ARRAY_INDEX I)))
									 (!ASSIGN (!CONCAT T
											   (!ARRAY_INDEX
											    (!MINUS K N)))
 										  K))
								 (!ASSIGN N (!PLUS N 1)))))
				   (!ASSIGN J (!CONCAT JA (!ARRAY_INDEX K)))
				   (!ASSIGN I (!CONCAT IA (!ARRAY_INDEX K))))
			   ((!AND (!LE 0 (!PLUS N (!MULT -1 G0770)))
				  (!LE (!PLUS N (!MULT -1 G0770)) (!PLUS K (!MULT -1 G0768)))
				  (!LE 0 (!PLUS C (!MULT -1 G0769)))
				  (!LE (!PLUS C (!MULT -1 G0769)) (!PLUS K (!MULT -1 G0768)))
				  (!LE G0768 K))
			    ((G0770 . N) (G0769 . C) (G0768 . K))))
		   (!ASSIGN K_FORHIGH E)
		   (!ASSIGN K K_FORLOW)
		   (!ASSIGN K_FORLOW 1)))
      (!COMMENT (DEF VA))
      (!IF (!LE 1 V)
	   (!BEGIN (!SIMPLE-ASSIGN K K_FORUNDEFINED)
		   (!WHILE (!AND (DEFRANGE 1 (!PLUS K -1) VA) (!LE K_FORLOW K) (!LE K (!PLUS K_FORHIGH 1)))
			   (!LE K K_FORHIGH)
			   (!BEGIN (!ASSIGN K (!PLUS K 1)) (!ASSIGN (!CONCAT VA (!ARRAY_INDEX K)) 0))
			   ((!LE G0745 K) ((G0745 . K))))
		   (!ASSIGN K_FORHIGH V)
		   (!ASSIGN K K_FORLOW)
		   (!ASSIGN K_FORLOW 1)))
      (!ASSIGN N 0)
      (!ASSIGN C 0)
      (!ASSUME (!AND (DEF E) (DEF V) (!LE 1 E) (!LE 1 V)))) 
VALUE)

NIL